package kodkod.analysis.ast;

import java.io.PrintWriter;
import java.util.*;

import kodkod.analysis.*;
import kodkod.analysis.ordering.*;
import kodkod.ast.*;
import kodkod.ast.operator.*;
import kodkod.ast.visitor.*;

public class wGraph extends Graph {
	
	public wNode root;
	
	Problem problem;
	
	GraphVisitorDOT2 visitor;
	
	public static boolean enableIsomorphicReduction = true;
	public static boolean enableRemoveStaticPaths = false;
		
	public wGraph(Problem problem) {
		super();
		this.problem = problem;
		this.visitor = new GraphVisitorDOT2(this);
		visitor.visit(problem.getFormula());
		
		if (enableIsomorphicReduction) isomorphicReduction();
		if (enableRemoveStaticPaths) removeStatic();
		
		Analyzer analyzer = new Analyzer(problem.getTranslation(new DefaultOrdering()));
		Collection<LeafInfo> nodeInfos = Analyzer.initialAnalysis.leafInfos.values();
		for (LeafInfo info : nodeInfos) {
			wNode node = getNode(info.leaf);
			
			HashMap<Variable,Relation> skolem = Analyzer.translation.skolemRelations;
			if (skolem.containsValue(info.leaf)) {
				for (Variable v : Analyzer.translation.skolemRelations.keySet()) if (skolem.get(v) == info.leaf) {
					node = getNode(v);	
				}
			}
			
			node.weight = info.getWeight();
			node.primaryIndex = info.index;
			node.primary = true;
		}
	}
	
	
	private boolean isomorphic(wNode n1, wNode n2) {
		if (n1.node.getClass() == n2.node.getClass()) {
			if (n1.node instanceof BinaryExpression) {
				BinaryExpression e1 = (BinaryExpression)n1.node;
				BinaryExpression e2 = (BinaryExpression)n2.node;
				if (e1.op() == e2.op() && getNode(e1.left()) == getNode(e2.left()) && getNode(e1.right()) == getNode(e2.right())) {
					return true;
				}
			} 
			else if (n1.node instanceof UnaryExpression) {
				UnaryExpression e1 = (UnaryExpression)n1.node;
				UnaryExpression e2 = (UnaryExpression)n2.node;
				if (e1.op() == e2.op() && getNode(e1.expression()) == getNode(e2.expression())) {
					return true;
				}
			}
			else if (n1.node instanceof ComparisonFormula) {
				ComparisonFormula f1 = (ComparisonFormula)n1.node;
				ComparisonFormula f2 = (ComparisonFormula)n2.node;
				if (f1.op() == ExprCompOperator.EQUALS && f2.op() == ExprCompOperator.EQUALS) {
					if (getNode(f1.left()) == getNode(f2.left()) && getNode(f1.right()) == getNode(f2.right()) ||
						getNode(f1.right()) == getNode(f2.left()) && getNode(f1.left()) == getNode(f2.right())
					) {
						return true;
					}	
				} else if (f1.op() == f2.op()){
					if (getNode(f1.left()) == getNode(f2.left()) && getNode(f1.right()) == getNode(f2.right())) {
						return true;
					}
				}
			}
		}
		return false;
	}
	
	private void isomorphicReduction() {
		// iterate bottom-up
		TreeSet<wNode> nodeList = new TreeSet<wNode>();
		nodeList.addAll(leafNodes);
		
		while (nodeList.size() > 0) {
			wNode node = nodeList.pollFirst();
			TreeSet<wEdge> edgeList = new TreeSet<wEdge>();
			edgeList.addAll(node.getIncomingEdges());
					
			// iterate parents
			while (edgeList.size() > 0) {
				wEdge edge1 = edgeList.pollFirst();
				wNode parent1 = edge1.node1;
				
				// compare to other parents
				if (getAllEdges().contains(edge1))
				for (wEdge edge2 : edgeList) {					
					wNode parent2 = edge2.node1;
					
					// check if the two parents are isomorphic (share the same node-type and children)
					// , eliminate one, and redirect incoming edges
					if (getAllEdges().contains(edge2) && parent1 != parent2)
					if (isomorphic(parent1, parent2)) {
						// redirect parent2's incoming edges to parent1							
						for (wEdge edgeToRedirect : parent2.getIncomingEdges()) {
							wEdge redirectedEdge = newEdge(edgeToRedirect.node1, parent1);
							redirectedEdge.color = edgeToRedirect.color;
						}
						replaceNode(parent2, parent1);
					}
				}
				nodeList.add(parent1);
			}
		}
	}
	
	private TreeSet<wEdge> getSubTree(wEdge topLevelEdge) {
		TreeSet<wEdge> subTree = new TreeSet<wEdge>();
		TreeSet<wEdge> recurse = new TreeSet<wEdge>();
		subTree.add(topLevelEdge);
		recurse.add(topLevelEdge);
		while (recurse.size() > 0) {
			wEdge check = recurse.pollFirst();
			
			for (wEdge edge : check.node2.getOutgoingEdges()) {
				subTree.add(edge);
				recurse.add(edge);
			}
		}
		return subTree;
	}
	
	private boolean removeStatic() {
		TreeSet<wNode> openNodes = getOpenNodes();
		TreeSet<wEdge> edgesToRemove = new TreeSet<wEdge>();
		for (wEdge edge : getAllEdges()) {
			if (!openNodes.contains(edge.node2)) {
				edgesToRemove.addAll(getSubTree(edge));
			}
		}
		if (edgesToRemove.size() > 0) {
			removeEdges(edgesToRemove);
			return true;
		} else {
			return false;
		}
	}
	
	public TreeSet<wEdge> getAllEdges() {
		return allEdges;
	}
	
	public wCompoundNode getCompoundNode(Node node) {
		wCompoundNode wn = new wCompoundNode(this, node);
		
		wNode existing = allNodes.get(wn);
		wCompoundNode uniqueWN = null;
		
		if (existing instanceof wCompoundNode) {
			uniqueWN = (wCompoundNode)existing;
		} else if (existing != null) {
			allNodes.remove(existing);
		}
		
		if (uniqueWN == null) {
			allNodes.put(wn, wn);
			return wn;
		} else {
			return uniqueWN;
		}
	}
	
	public TreeSet<wNode> getOpenNodes() {
		TreeSet<wEdge> edgeList = new TreeSet<wEdge>();
		TreeSet<wNode> nodeList = new TreeSet<wNode>();
		for (wNode node : leafNodes) {
			if (node.primary) {
				nodeList.add(node);
				edgeList.addAll(node.getIncomingEdges());
			}
		}
		while (edgeList.size() > 0) {
			wEdge edge = edgeList.pollFirst();
			nodeList.add(edge.node1);
			edgeList.addAll(edge.node1.getIncomingEdges());
		}
		return nodeList;
	}

	public void printInfo(PrintWriter writer) {
		for (wNode node : leafNodes) if (node.primary) {
			String label = node.getLabel();
			label = label.replaceAll("\\\\n", "");
			writer.write(label + "\n");
		}
		writer.println();
	}
	
	public void printGraph(PrintWriter writer) {
		TreeSet<wNode> openNodes = getOpenNodes();					
		TreeSet<wNode> done = new TreeSet<wNode>();
		
		writer.println("digraph AST {");
		
		writer.println("label=\""+problem+"\"");
		
		for (wEdge edge : allEdges) {
			wNode probe = getNode(edge.node1);
			if (probe.compound != null) {
				probe = probe.compound;
			}
			if (done.add(probe)) {
				if (!openNodes.contains(probe)) probe.fillcolor = "#aaccff";
				writer.println(probe.toString());
			}
			probe = getNode(edge.node2);
			if (probe.compound != null) {
				probe = probe.compound;
			}
			if (done.add(probe)) {
				if (!openNodes.contains(probe)) probe.fillcolor = "#aaccff";
				writer.println(probe.toString());
			}
			writer.println(edge.toString());
		}
		
		writer.println("}");
		writer.flush();
	}
}